0.00/0.34	NO
0.00/0.35	
0.00/0.35	Problem:
0.00/0.35	 f x x -> a
0.00/0.35	 f x (s x) -> b
0.00/0.35	 mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.35	
0.00/0.35	Proof:
0.00/0.35	 Higher-Order Church Rosser Processor:
0.00/0.35	  f x x -> a
0.00/0.35	  f x (s x) -> b
0.00/0.35	  mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.35	  critical peaks: 0
0.00/0.35	   
0.00/0.35	   
0.00/0.35	   Redundant Rules Transformation for Pattern Rewrite Systems:
0.00/0.35	    f x x -> a
0.00/0.35	    f x (s x) -> b
0.00/0.35	    mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.35	    mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
0.00/0.35	    f (mu (\x. s x)) (mu (\x. s x)) -> b
0.00/0.35	    Higher-Order Church Rosser Processor:
0.00/0.35	     f x x -> a
0.00/0.35	     f x (s x) -> b
0.00/0.35	     mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.35	     mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
0.00/0.35	     f (mu (\x. s x)) (mu (\x. s x)) -> b
0.00/0.35	     critical peaks: 8
0.00/0.35	      a <-[]-> b
0.00/0.35	      105 (mu (\x. 105 x)) <-[]-> 105 (105 (mu (\x. 105 x)))
0.00/0.35	      f (s (mu (\x. s x))) (mu (\x. s x)) <-[0,1]-> b
0.00/0.35	      f (mu (\x. s x)) (s (mu (\x. s x))) <-[1]-> b
0.00/0.35	      115 (115 (mu (\x. 115 x))) <-[]-> 115 (mu (\x. 115 x))
0.00/0.35	      f (s (s (mu (\x. s x)))) (mu (\x. s x)) <-[0,1]-> b
0.00/0.35	      f (mu (\x. s x)) (s (s (mu (\x. s x)))) <-[1]-> b
0.00/0.35	      b <-[]-> a
0.00/0.35	      
0.00/0.35	      Higher-Order Nonconfluence Processor:
0.00/0.35	       non-joinable conversion:
0.00/0.35	       a *<- a <- f (mu (\x. s x)) (mu (\x. s x)) -> b ->* b
0.00/0.35	       Qed
0.00/0.35	 
0.00/0.35	EOF